sorted(L) == i:int_seg(0; ||L||), j:int_seg(0; i). L[j]  L[i] 

latex

Definitions	||as||, x:A. B(x), int_seg(i; j), #$n, A  B, l[i]
FDL editor aliases	sorted